the_es:ES, e', e:E, l:IdLnk. (e  rcvs(l;before(e')))  ((e <loc e') & (haslnk(l;e))) 

latex

Definitions	x:A. B(x), P  Q, rcvs(l;before(e')), P & Q, P  Q, , P  Q, t  T
Lemmas	iff functionality wrt iff, l member wf, filter wf, es-haslnk wf, es-before wf, assert wf, es-locl wf, member filter, and functionality wrt iff, member-es-before, IdLnk wf, es-E wf, event system wf